/*
   Copyright (c) 2012, 2015 Mizar Tools Contributors (mizartools.org)

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*/
/*  Contributors :
 *	2012-04-14 Marco Riccardi - initial implementation
 *  2015-01-11 Marco Riccardi - filter Verum theorem
 *                            - changed getSchemeList in getElementList
 *  
 */
package org.mizartools.example.ui;

import java.awt.BorderLayout;
import java.awt.Dimension;
import java.awt.event.ActionEvent;
import java.io.File;
import java.util.Calendar;
import java.util.LinkedList;

import javax.swing.AbstractAction;
import javax.swing.JButton;
import javax.swing.JPanel;
import javax.swing.JProgressBar;
import javax.swing.JScrollPane;
import javax.swing.JTextArea;

import org.mizartools.dli.AggregateNotation;
import org.mizartools.dli.ArticleId;
import org.mizartools.dli.AttributeNotation;
import org.mizartools.dli.DecodedLibraryItem;
import org.mizartools.dli.DliException;
import org.mizartools.dli.ForgNotation;
import org.mizartools.dli.FunctorNotation;
import org.mizartools.dli.ItemDefinition;
import org.mizartools.dli.ModeNotation;
import org.mizartools.dli.PredicateNotation;
import org.mizartools.dli.SelectorNotation;
import org.mizartools.dli.StructureNotation;
import org.mizartools.dli.SymbolId;
import org.mizartools.dli.utility.ItemError;
import org.mizartools.dli.utility.ItemFactory;
import org.mizartools.dli.utility.SchemeId;
import org.mizartools.dli.utility.TheoremId;
import org.mizartools.system.Article;
import org.mizartools.system.ArticleFactory;
import org.mizartools.system.EnvironFile;
import org.mizartools.system.IClusterRegistration;
import org.mizartools.system.IElement;
import org.mizartools.system.ListArticleFile;
import org.mizartools.system.utility.ConstructorsSignature;
import org.mizartools.system.utility.DefinientiaSignature;
import org.mizartools.system.utility.IdentifyRegistrationsSignature;
import org.mizartools.system.utility.NotationsSignature;
import org.mizartools.system.utility.PropertyRegistrationsSignature;
import org.mizartools.system.utility.ReductionRegistrationsSignature;
import org.mizartools.system.utility.RegistrationsSignature;
import org.mizartools.system.utility.SchemesSignature;
import org.mizartools.system.utility.TheoremsSignature;
import org.mizartools.system.xml.Canceled;
import org.mizartools.system.xml.Constructor;
import org.mizartools.system.xml.Definiens;
import org.mizartools.system.xml.Identify;
import org.mizartools.system.xml.Pattern;
import org.mizartools.system.xml.Property;
import org.mizartools.system.xml.Reduction;
import org.mizartools.system.xml.Scheme;
import org.mizartools.system.xml.Theorem;
import org.mizartools.utility.UtilityFile;

@SuppressWarnings("serial")
public class TestDLIPanel extends JPanel {

	private JTextArea textArea;
	private JScrollPane scroller;
	private JPanel progressBarPanel;
	private JProgressBar progressBarMML;
	private JProgressBar progressBarVerifier;
	private JButton button;
	private TestFrame testFrame;

	public TestDLIPanel(TestFrame testFrame){
		super();
		this.testFrame = testFrame;
    	setLayout(new BorderLayout());
		setPreferredSize(new Dimension(500, 150));
		button = new JButton();
		AbstractAction action =  new AbstractAction() { 
	 	    public void actionPerformed(ActionEvent e) {
	 	    	textArea.setText(Calendar.getInstance().getTime().toString()+"\n\n");
	 	    	TestDLIPanel.Job job = new TestDLIPanel.Job();
	 			Thread thread = new Thread(job);
	 			thread.start();
	 	    } 
	 	}; 
	 	button.setAction(action);
	 	button.setMaximumSize(getMaximumSize());
	 	button.setText("Start");
		add(button, BorderLayout.NORTH);
		textArea = new JTextArea();
		textArea.setEditable(false);
        scroller = new JScrollPane();
		scroller.getViewport().add(textArea);
		add(scroller, BorderLayout.CENTER);
		
		progressBarPanel = new JPanel();
		progressBarPanel.setLayout(new BorderLayout());
		progressBarVerifier = new JProgressBar();
		progressBarPanel.add(progressBarVerifier, BorderLayout.NORTH);
		progressBarMML = new JProgressBar();
		progressBarPanel.add(progressBarMML, BorderLayout.SOUTH);
		add(progressBarPanel,BorderLayout.SOUTH);
	}
	
	private class Job implements Runnable {

		private String dliPath = EnvironFile.getMIZFILES() + File.separator + "dli";
		
		@Override
		public void run() {
			button.setEnabled(false);
			File dliDirectory = new File(dliPath);
			if (!dliDirectory.exists()){
	    		textArea.append("\n");
	    		textArea.append(dliPath);
	    		textArea.append(" is not present.\nThis is not a content of Mizar System.\nIf you want test MML against DLI files,\nyou can download the necessary files\nfrom \"mmlquery.mizar.org\".");
	    		textArea.append("\n");
	    		textArea.repaint();
	    		textArea.setCaretPosition(textArea.getText().length()-1);
	    		return;
			}

			LinkedList<String> articleList = ListArticleFile.getAllArticleList();
	    	progressBarMML.setMaximum(articleList.size()+1);
	    	progressBarMML.setValue(0);
	    	progressBarMML.setIndeterminate(false);
	    	progressBarVerifier.setMaximum(100);
	    	progressBarVerifier.setValue(0);
			progressBarVerifier.setIndeterminate(false);
	    	Article article = null;
	    	String fileName = null;
	    	int progress = 0;
			try {
				Boolean error = false;
				for (String aid : articleList){
					progress++;
		    		if (progress < 0) continue;
		    		if (!error){
			    		article = ArticleFactory.getInstance().getArticle(aid);
						textArea.append((article.getAid()+"["+String.valueOf(progress)+"]        ").substring(0,14)+" : ");
			    		textArea.repaint();
			    		textArea.setCaretPosition(textArea.getText().length()-1);
			    		/* test parser */
			    		File dliFile = new File(dliPath, aid.toLowerCase()+".dli");
			    		String text = UtilityFile.readFile(dliFile);
			    		String arrayText[] = text.split("\n");
			    		error = checkParser(arrayText);
		    			/* test xml dli converter */
		    			Article articleXml = ArticleFactory.getInstance().getArticle(aid);
			    		boolean arrayFound[] = new boolean[arrayText.length];
		    			if (!error) error = checkConstructors(articleXml, arrayText, arrayFound);
		    			if (!error) error = checkNotations(articleXml, arrayText, arrayFound);  
		    			if (!error) error = checkDefinientia(articleXml, arrayText, arrayFound);
		    			if (!error) error = checkRegistrations(articleXml, arrayText, arrayFound);
		    			if (!error) error = checkIdentifyRegistrations(articleXml, arrayText, arrayFound);
		    			if (!error) error = checkReductionRegistrations(articleXml, arrayText, arrayFound);
		    			if (!error) error = checkPropertyRegistrations(articleXml, arrayText, arrayFound);
		    			if (!error) error = checkTheorems(articleXml, arrayText, arrayFound);
		    			if (!error) error = checkSchemes(articleXml, arrayText, arrayFound);
		    			if (!error) {
			    			for (int i = 0 ; i<arrayFound.length ; i++){
			    				if (!arrayFound[i]){
			    					if (ItemError.isWithError(arrayText[i])) continue;
			    					error = true;
									textArea.append("\n");
			    	    			textArea.append("--NOT FOUND--");
									textArea.append("\n");
			    	    			textArea.append(arrayText[i]);
									textArea.append("\n");
			    	    			textArea.append("--NOT FOUND--");
									textArea.append("\n");
			    				}
			    			}
		    			}
		    			if (error) {
		    				error = false;
		    				textArea.append(" [ERROR]");
		    			} else {
		    				textArea.append(" [OK]");
		    			}
		    				
						textArea.append("\n");
			    		textArea.repaint();
			    		textArea.setCaretPosition(textArea.getText().length()-1);
				    	progressBarMML.setValue(progress);
				    	progressBarMML.repaint();
				    	if (testFrame.isClosed()) {
				    		error = true;
				    	}
		    		}
		    	}
			} 
			catch (Exception e) {
				textArea.append("\n");
	    		textArea.append(fileName);
	    		textArea.append(" -> Error");
				textArea.append("\n");
				textArea.append(e.getMessage());
				textArea.append("\n");
	    		textArea.repaint();
	    		textArea.setCaretPosition(textArea.getText().length()-1);
			}
			textArea.append("\n");
			textArea.repaint();
			textArea.setCaretPosition(textArea.getText().length()-1);
	    	progressBarMML.setValue(0);
			button.setEnabled(true);
		}
		
	}

	private boolean checkParser(String arrayText[]) {
		boolean error = false;
		for (int i = 0; i<arrayText.length; i++){
			String inputLine = arrayText[i];
			if (!ItemError.isWithError(inputLine)){
				try {
					String inputLineParsed = DecodedLibraryItem.newInstance(inputLine).toString(); 
					if (!inputLineParsed.equals(inputLine)){
						textArea.append("\n");
						textArea.append("--ERROR--line["+i+"]");
						textArea.append("\n");
						textArea.append(inputLine);
						textArea.append("\n");
						textArea.append(inputLineParsed);
						textArea.append("\n");
						textArea.append("--ERROR--");
						textArea.append("\n");
						error = true;
					}
				}
				catch (Exception e) {
					textArea.append("\n");
					textArea.append("--PARSED ERROR ON --line["+i+"]");
					textArea.append("\n");
					textArea.append(e.getMessage());
					textArea.append("\n");
					textArea.append(inputLine);
					textArea.append("\n");
					textArea.append("--ERROR--");
					textArea.append("\n");
					error = true;
				}
			}
		}
		if (!error) {
			textArea.append("[PARSED]");
		}
		return error;
	}
	
	private boolean checkConstructors(Article articleXml, String arrayText[], boolean arrayFound[]) throws DliException {
		boolean error = false;
		if (articleXml.hasConstructors()){
			ConstructorsSignature constructorsSignature = articleXml.getConstructorsSignature();
			for (Constructor constructor : articleXml.getConstructors().getConstructorList()){
				DecodedLibraryItem decodedLibraryItem = ItemFactory.getItem(constructorsSignature, constructor);
				String dliFromXml = decodedLibraryItem.toString();
				String resourceId = decodedLibraryItem.getItemId().toString()+"=";
				boolean found = false; 
    			for (int i = 0 ; i<arrayText.length ; i++){
    				if (arrayText[i].startsWith(resourceId)){
    					found = true;
    					if (!arrayText[i].equals(dliFromXml)) {
							error = true;
							textArea.append("\n");
	    	    			textArea.append("--ERROR CONSTRUCTOR--");
							textArea.append("\n");
	    	    			textArea.append(constructor.getXMLElementList().toString());
							textArea.append("\n");
	    	    			textArea.append("xml="+dliFromXml);
							textArea.append("\n");
		    				textArea.append("dli="+arrayText[i]);
							textArea.append("\n");
	    	    			textArea.append("--ERROR--");
							textArea.append("\n");
    					}
    					arrayFound[i] = true;
    				}
    			}
    			if (!found) {
    				error = true;
					textArea.append("\n");
	    			textArea.append("--NOT FOUND CONSTRUCTOR--");
					textArea.append("\n");
	    			textArea.append(dliFromXml);
					textArea.append("\n");
	    			textArea.append("--NOT FOUND--");
					textArea.append("\n");
    			}
			}
			if (!error) {
				textArea.append("[CONSTRUCTORS]");
			}
		}
		return error;
	}

	private DecodedLibraryItem changeSymbolWithUnknown(DecodedLibraryItem decodedLibraryItem) throws DliException {
		ItemDefinition itemDefinition = decodedLibraryItem.getItemDefinition();
		ArticleId articleId = new ArticleId("UNKNOWN");
		if (itemDefinition instanceof org.mizartools.dli.AttributeNotation) {
			AttributeNotation attributeNotation = (AttributeNotation)itemDefinition;
			SymbolId symbolId = attributeNotation.getSymbolId();
			SymbolId symbolIdNew = new SymbolId(articleId, symbolId.getSymbolType(), symbolId.getToken1(), symbolId.getToken2(), 1);
			itemDefinition = new AttributeNotation(symbolIdNew, attributeNotation.getLoci(), attributeNotation.getFormat(), attributeNotation.getVisible(), attributeNotation.getConstructor(), attributeNotation.getAntonym(), attributeNotation.getSynonym());
		} else if (itemDefinition instanceof org.mizartools.dli.AggregateNotation) {
			AggregateNotation aggregateNotation = (AggregateNotation)itemDefinition;
			SymbolId symbolId = aggregateNotation.getSymbolId();
			SymbolId symbolIdNew = new SymbolId(articleId, symbolId.getSymbolType(), symbolId.getToken1(), symbolId.getToken2(), 1);
			itemDefinition = new AggregateNotation(symbolIdNew, aggregateNotation.getLoci(), aggregateNotation.getFormat(), aggregateNotation.getVisible(), aggregateNotation.getConstructor(), aggregateNotation.getSynonym());
		} else if (itemDefinition instanceof org.mizartools.dli.PredicateNotation) {
			PredicateNotation predicateNotation = (PredicateNotation)itemDefinition;
			SymbolId symbolId = predicateNotation.getSymbolId();
			SymbolId symbolIdNew = new SymbolId(articleId, symbolId.getSymbolType(), symbolId.getToken1(), symbolId.getToken2(), 1);
			itemDefinition = new PredicateNotation(symbolIdNew, predicateNotation.getLoci(), predicateNotation.getFormat(), predicateNotation.getVisible(), predicateNotation.getConstructor(), predicateNotation.getAntonym(), predicateNotation.getSynonym());
		} else if (itemDefinition instanceof org.mizartools.dli.ModeNotation) {
			ModeNotation modeNotation = (ModeNotation)itemDefinition;
			SymbolId symbolId = modeNotation.getSymbolId();
			SymbolId symbolIdNew = new SymbolId(articleId, symbolId.getSymbolType(), symbolId.getToken1(), symbolId.getToken2(), 1);
			itemDefinition = new ModeNotation(symbolIdNew, modeNotation.getLoci(), modeNotation.getFormat(), modeNotation.getVisible(), modeNotation.getConstructor(), modeNotation.getAbbreviation(), modeNotation.getSynonym());
		} else if (itemDefinition instanceof org.mizartools.dli.ForgNotation) {
			ForgNotation forgNotation = (ForgNotation)itemDefinition;
			SymbolId symbolId = forgNotation.getSymbolId();
			SymbolId symbolIdNew = new SymbolId(articleId, symbolId.getSymbolType(), symbolId.getToken1(), symbolId.getToken2(), 1);
			itemDefinition = new ForgNotation(symbolIdNew, forgNotation.getLoci(), forgNotation.getFormat(), forgNotation.getVisible(), forgNotation.getConstructor(), forgNotation.getSynonym());
		} else if (itemDefinition instanceof org.mizartools.dli.SelectorNotation) {
			SelectorNotation selectorNotation = (SelectorNotation)itemDefinition;
			SymbolId symbolId = selectorNotation.getSymbolId();
			SymbolId symbolIdNew = new SymbolId(articleId, symbolId.getSymbolType(), symbolId.getToken1(), symbolId.getToken2(), 1);
			itemDefinition = new SelectorNotation(symbolIdNew, selectorNotation.getLoci(), selectorNotation.getFormat(), selectorNotation.getVisible(), selectorNotation.getConstructor(), selectorNotation.getSynonym());
		} else if (itemDefinition instanceof org.mizartools.dli.StructureNotation) {
			StructureNotation structureNotation = (StructureNotation)itemDefinition;
			SymbolId symbolId = structureNotation.getSymbolId();
			SymbolId symbolIdNew = new SymbolId(articleId, symbolId.getSymbolType(), symbolId.getToken1(), symbolId.getToken2(), 1);
			itemDefinition = new StructureNotation(symbolIdNew, structureNotation.getLoci(), structureNotation.getFormat(), structureNotation.getVisible(), structureNotation.getConstructor(), structureNotation.getSynonym());
		} else if (itemDefinition instanceof org.mizartools.dli.FunctorNotation) {
			FunctorNotation functorNotation = (FunctorNotation)itemDefinition;
			SymbolId symbolId1 = functorNotation.getSymbolId1();
			SymbolId symbolIdNew1 = new SymbolId(articleId, symbolId1.getSymbolType(), symbolId1.getToken1(), symbolId1.getToken2(), 1);
			SymbolId symbolId2 = functorNotation.getSymbolId2();
			SymbolId symbolIdNew2 = null;
			if (symbolId2 != null) {
				symbolIdNew2 = new SymbolId(articleId, symbolId2.getSymbolType(), symbolId2.getToken1(), symbolId2.getToken2(), 1);
			}
			itemDefinition = new FunctorNotation(symbolIdNew1, symbolIdNew2, functorNotation.getLoci(), functorNotation.getFormat(), functorNotation.getVisible(), functorNotation.getConstructor(), functorNotation.getSynonym());
		}
		return new DecodedLibraryItem(decodedLibraryItem.getItemId(), itemDefinition); 
	}
	
	private boolean checkNotations(Article articleXml, String arrayText[], boolean arrayFound[]) throws DliException {
		boolean error = false;
		if (articleXml.hasNotations()){
			NotationsSignature notationsSignature = articleXml.getNotationsSignature();
			for (Pattern pattern : articleXml.getNotations().getPatternList()){
				DecodedLibraryItem decodedLibraryItem = ItemFactory.getItem(notationsSignature, pattern);
				String dliFromXml = decodedLibraryItem.toString();
				String resourceId = decodedLibraryItem.getItemId().toString()+"=";
				boolean found = false; 
    			for (int i = 0 ; i<arrayText.length ; i++){
    				if (arrayText[i].startsWith(resourceId)){
    					found = true;
						if (arrayText[i].contains("UNKNOWN")) {
							dliFromXml = changeSymbolWithUnknown(decodedLibraryItem).toString();
						}
    					if (!arrayText[i].equals(dliFromXml)) {
    						if (!ItemError.isWithError(dliFromXml)) {
    							error = true;
    							textArea.append("\n");
    	    	    			textArea.append("--ERROR NOTATION--");
    							textArea.append("\n");
    	    	    			textArea.append(pattern.getXMLElementList().toString());
    							textArea.append("\n");
    	    	    			textArea.append("xml="+dliFromXml);
    							textArea.append("\n");
    		    				textArea.append("dli="+arrayText[i]);
    							textArea.append("\n");
    	    	    			textArea.append("--ERROR--");
    							textArea.append("\n");	
    						}
    					}
    					arrayFound[i] = true;
    				}
    			}
    			if (!found) {
    				error = true;
					textArea.append("\n");
	    			textArea.append("--NOT FOUND NOTATION--");
					textArea.append("\n");
	    			textArea.append(dliFromXml);
					textArea.append("\n");
	    			textArea.append("--NOT FOUND--");
					textArea.append("\n");
    			}
			}
			if (!error) {
				textArea.append("[NOTATIONS]");
			}
		}
		return error;
	}

	private boolean checkDefinientia(Article articleXml, String arrayText[], boolean arrayFound[]) throws DliException {
		boolean error = false;
		if (articleXml.hasDefinientia()){
			DefinientiaSignature definientiaSignature = articleXml.getDefinientiaSignature();
			int relativeNr = 0;
			int nrDefiniens = 0;
			for (Definiens definiens : articleXml.getDefinientia().getDefiniensList()){
				nrDefiniens++;
				relativeNr = definiens.getDefnr() - nrDefiniens;
				DecodedLibraryItem decodedLibraryItem = ItemFactory.getItem(definientiaSignature, definiens, relativeNr);
				String dliFromXml = decodedLibraryItem.toString();
				String resourceId = decodedLibraryItem.getItemId().toString()+"=";
				boolean found = false; 
    			for (int i = 0 ; i<arrayText.length ; i++){
    				if (arrayText[i].startsWith(resourceId)){
    					found = true;
    					if (!arrayText[i].equals(dliFromXml)) {
		    				error = true;
							textArea.append("\n");
	    	    			textArea.append("--ERROR DEFINIENTIA--");
							textArea.append("\n");
	    	    			textArea.append(definiens.getXMLElementList().toString());
							textArea.append("\n");
	    	    			textArea.append("xml="+dliFromXml);
							textArea.append("\n");
		    				textArea.append("dli="+arrayText[i]);
							textArea.append("\n");
	    	    			textArea.append("--ERROR--");
							textArea.append("\n");
    					}
    					arrayFound[i] = true;
    				}
    			}
    			if (!found) {
    				error = true;
					textArea.append("\n");
	    			textArea.append("--NOT FOUND DEFINIENTIA--");
					textArea.append("\n");
	    			textArea.append(dliFromXml);
					textArea.append("\n");
	    			textArea.append("--NOT FOUND--");
					textArea.append("\n");
    			}
			}
			if (!error) {
				textArea.append("[DEFINIENTIA]");
			}
		}
		return error;
	}

	private boolean checkRegistrations(Article articleXml, String arrayText[], boolean arrayFound[]) throws DliException {
		boolean error = false;
		if (articleXml.hasRegistrations()){
			RegistrationsSignature registrationsSignature = articleXml.getRegistrationsSignature();
			for (IClusterRegistration iClusterRegistration : articleXml.getRegistrations().getIClusterRegistrationList()){
				DecodedLibraryItem decodedLibraryItem = null;
				decodedLibraryItem = ItemFactory.getItem(registrationsSignature, iClusterRegistration);
				
				String dliFromXml = decodedLibraryItem.toString();
				String resourceId = decodedLibraryItem.getItemId().toString()+"=";
				boolean found = false; 
    			for (int i = 0 ; i<arrayText.length ; i++){
    				if (arrayText[i].startsWith(resourceId)){
    					found = true;
    					if (!arrayText[i].equals(dliFromXml)) {
		    				error = true;
							textArea.append("\n");
	    	    			textArea.append("--ERROR REGISTRATION--");
							textArea.append("\n");
	    	    			textArea.append(iClusterRegistration.getXMLElementList().toString());
							textArea.append("\n");
	    	    			textArea.append("xml="+dliFromXml);
							textArea.append("\n");
		    				textArea.append("dli="+arrayText[i]);
							textArea.append("\n");
	    	    			textArea.append("--ERROR--");
							textArea.append("\n");
    					}
    					arrayFound[i] = true;
    				}
    			}
    			if (!found) {
    				error = true;
					textArea.append("\n");
	    			textArea.append("--NOT FOUND REGISTRATION--");
					textArea.append("\n");
	    			textArea.append(dliFromXml);
					textArea.append("\n");
	    			textArea.append("--NOT FOUND--");
					textArea.append("\n");
    			}
			}
			if (!error) {
				textArea.append("[REGISTRATION]");
			}
		}
		return error;
	}

	private boolean checkIdentifyRegistrations(Article articleXml, String arrayText[], boolean arrayFound[]) throws DliException {
		boolean error = false;
		if (articleXml.hasIdentifyRegistrations()){
			IdentifyRegistrationsSignature identifyRegistrationsSignature = articleXml.getIdentifyRegistrationsSignature();
			for (Identify identify : articleXml.getIdentifyRegistrations().getIdentifyList()){
				DecodedLibraryItem decodedLibraryItem = null;
				decodedLibraryItem = ItemFactory.getItem(identifyRegistrationsSignature, identify);
				
				String dliFromXml = decodedLibraryItem.toString();
				String resourceId = decodedLibraryItem.getItemId().toString()+"=";
				boolean found = false; 
    			for (int i = 0 ; i<arrayText.length ; i++){
    				if (arrayText[i].startsWith(resourceId)){
    					found = true;
    					if (!arrayText[i].equals(dliFromXml)) {
							error = true;
							textArea.append("\n");
	    	    			textArea.append("--ERROR IDENTIFY REGISTRATION--");
							textArea.append("\n");
	    	    			textArea.append(identify.getXMLElementList().toString());
							textArea.append("\n");
	    	    			textArea.append("xml="+dliFromXml);
							textArea.append("\n");
		    				textArea.append("dli="+arrayText[i]);
							textArea.append("\n");
	    	    			textArea.append("--ERROR--");
							textArea.append("\n");
    					}
    					arrayFound[i] = true;
    				}
    			}
    			if (!found) {
    				error = true;
					textArea.append("\n");
	    			textArea.append("--NOT FOUND IDENTIFY REGISTRATION--");
					textArea.append("\n");
	    			textArea.append(dliFromXml);
					textArea.append("\n");
	    			textArea.append("--NOT FOUND--");
					textArea.append("\n");
    			}
			}
			if (!error) {
				textArea.append("[IDENTIFY-REGISTRATION]");
			}
		}
		return error;
	}

	private boolean checkPropertyRegistrations(Article articleXml, String arrayText[], boolean arrayFound[]) throws DliException {
		boolean error = false;
		if (articleXml.hasPropertyRegistrations()){
			PropertyRegistrationsSignature propertyRegistrationsSignature = articleXml.getPropertyRegistrationsSignature();
			for (Property property : articleXml.getPropertyRegistrations().getPropertyList()){
				DecodedLibraryItem decodedLibraryItem = null;
				decodedLibraryItem = ItemFactory.getItem(propertyRegistrationsSignature, property);
				
				String dliFromXml = decodedLibraryItem.toString();
				String resourceId = decodedLibraryItem.getItemId().toString()+"=";
				boolean found = false; 
    			for (int i = 0 ; i<arrayText.length ; i++){
    				if (arrayText[i].startsWith(resourceId)){
    					found = true;
    					if (!arrayText[i].equals(dliFromXml)) {
							error = true;
							textArea.append("\n");
	    	    			textArea.append("--ERROR PROPERTY REGISTRATION--");
							textArea.append("\n");
	    	    			textArea.append(property.getXMLElementList().toString());
							textArea.append("\n");
	    	    			textArea.append("xml="+dliFromXml);
							textArea.append("\n");
		    				textArea.append("dli="+arrayText[i]);
							textArea.append("\n");
	    	    			textArea.append("--ERROR--");
							textArea.append("\n");
    					}
    					arrayFound[i] = true;
    				}
    			}
    			if (!found) {
    				error = true;
					textArea.append("\n");
	    			textArea.append("--NOT FOUND PROPERTY REGISTRATION--");
					textArea.append("\n");
	    			textArea.append(dliFromXml);
					textArea.append("\n");
	    			textArea.append("--NOT FOUND--");
					textArea.append("\n");
    			}
			}
			if (!error) {
				textArea.append("[PROPERTY-REGISTRATION]");
			}
		}
		return error;
	}
	
	private boolean checkReductionRegistrations(Article articleXml, String arrayText[], boolean arrayFound[]) throws DliException {
		boolean error = false;
		if (articleXml.hasReductionRegistrations()){
			ReductionRegistrationsSignature reductionRegistrationsSignature = articleXml.getReductionRegistrationsSignature();
			for (Reduction reduction : articleXml.getReductionRegistrations().getReductionList()){
				DecodedLibraryItem decodedLibraryItem = null;
				decodedLibraryItem = ItemFactory.getItem(reductionRegistrationsSignature, reduction);
				
				String dliFromXml = decodedLibraryItem.toString();
				String resourceId = decodedLibraryItem.getItemId().toString()+"=";
				boolean found = false; 
    			for (int i = 0 ; i<arrayText.length ; i++){
    				if (arrayText[i].startsWith(resourceId)){
    					found = true;
    					if (!arrayText[i].equals(dliFromXml)) {
							error = true;
							textArea.append("\n");
	    	    			textArea.append("--ERROR REDUCTION REGISTRATION--");
							textArea.append("\n");
	    	    			textArea.append(reduction.getXMLElementList().toString());
							textArea.append("\n");
	    	    			textArea.append("xml="+dliFromXml);
							textArea.append("\n");
		    				textArea.append("dli="+arrayText[i]);
							textArea.append("\n");
	    	    			textArea.append("--ERROR--");
							textArea.append("\n");
    					}
    					arrayFound[i] = true;
    				}
    			}
    			if (!found) {
    				error = true;
					textArea.append("\n");
	    			textArea.append("--NOT FOUND REDUCTION REGISTRATION--");
					textArea.append("\n");
	    			textArea.append(dliFromXml);
					textArea.append("\n");
	    			textArea.append("--NOT FOUND--");
					textArea.append("\n");
    			}
			}
			if (!error) {
				textArea.append("[REDUCTION-REGISTRATION]");
			}
		}
		return error;
	}
	
	private boolean checkTheorems(Article articleXml, String arrayText[], boolean arrayFound[]) throws DliException {
		boolean error = false;
		if (articleXml.hasTheorems()){
			TheoremsSignature theoremsSignature = articleXml.getTheoremsSignature();
			TheoremId theoremId = new TheoremId();
			TheoremId theoremIdDef = new TheoremId();
			for (Theorem theorem : articleXml.getTheorems().getTheoremList()){
				if (theorem.getFormula() instanceof org.mizartools.system.xml.Verum) {
					if (theorem.getKind().name() == "T") theoremId.setId(theoremId.getId()+1);
					continue;
				}
				DecodedLibraryItem decodedLibraryItem = null;
				decodedLibraryItem = ItemFactory.getItem(theoremsSignature, theorem, theoremId, theoremIdDef);
				String dliFromXml = decodedLibraryItem.toString();
				String resourceId = decodedLibraryItem.getItemId().toString()+"=";
				boolean found = false; 
    			for (int i = 0 ; i<arrayText.length ; i++){
    				if (arrayText[i].startsWith(resourceId)){
    					found = true;
    					if (!ItemError.isWithError(dliFromXml)) {
	    					if (!arrayText[i].equals(dliFromXml)) {
			    				error = true;
								textArea.append("\n");
		    	    			textArea.append("--ERROR THEOREM--");
								textArea.append("\n");
		    	    			textArea.append(theorem.getXMLElementList().toString());
								textArea.append("\n");
		    	    			textArea.append("xml="+dliFromXml);
								textArea.append("\n");
			    				textArea.append("dli="+arrayText[i]);
								textArea.append("\n");
		    	    			textArea.append("--ERROR--");
								textArea.append("\n");
	    					}
    					}
    					arrayFound[i] = true;
    				}
    			}
    			if (!found) {
    				if (!ItemError.isWithError(dliFromXml)) {
	    				error = true;
						textArea.append("\n");
		    			textArea.append("--NOT FOUND THEOREM--");
						textArea.append("\n");
		    			textArea.append(dliFromXml);
						textArea.append("\n");
		    			textArea.append("--NOT FOUND--");
						textArea.append("\n");
					}
    			}
			}
			if (!error) {
				textArea.append("[THEOREMS]");
			}
		}
		return error;
	}

	private boolean checkSchemes(Article articleXml, String arrayText[], boolean arrayFound[]) throws DliException {
		boolean error = false;
		if (articleXml.hasSchemes()){
			SchemesSignature schemesSignature = articleXml.getSchemesSignature();
			SchemeId schemeId = new SchemeId();
			for (IElement element : articleXml.getSchemes().getElementList()){
				if (element instanceof Canceled) {
					// schemeId.increment();
				} else if (element instanceof Scheme) {
					Scheme scheme = (Scheme)element;
					DecodedLibraryItem decodedLibraryItem = null;
					decodedLibraryItem = ItemFactory.getItem(schemesSignature, scheme, schemeId);
					String dliFromXml = decodedLibraryItem.toString();
					String resourceId = decodedLibraryItem.getItemId().toString()+"=";
					boolean found = false; 
	    			for (int i = 0 ; i<arrayText.length ; i++){
	    				if (arrayText[i].startsWith(resourceId)){
	    					found = true;
	    					if (!arrayText[i].equals(dliFromXml)) {
			    				error = true;
								textArea.append("\n");
		    	    			textArea.append("--ERROR SCHEME--");
								textArea.append("\n");
		    	    			textArea.append(scheme.getXMLElementList().toString());
								textArea.append("\n");
		    	    			textArea.append("xml="+dliFromXml);
								textArea.append("\n");
			    				textArea.append("dli="+arrayText[i]);
								textArea.append("\n");
		    	    			textArea.append("--ERROR--");
								textArea.append("\n");
	    					}
	    					arrayFound[i] = true;
	    				}
	    			}
	    			if (!found) {
	    				error = true;
						textArea.append("\n");
		    			textArea.append("--NOT FOUND SCHEME--");
						textArea.append("\n");
		    			textArea.append(dliFromXml);
						textArea.append("\n");
		    			textArea.append("--NOT FOUND--");
						textArea.append("\n");
	    			}
				}
			}
			if (!error) {
				textArea.append("[SCHEMES]");
			}
		}
		return error;
	}
	
}
